%% -*- coding:utf-8; mode:erlang; erlang-indent-level: 2 -*-
{wpc_magnet_mask,
 [
  {mask_on_off,
   [
    {1,"Maskierung ausschalten"},
    {2,"Maskierung umschalten"},
    {3,"Maskierung Einschalten"}
   ]},
  {tools_menu_entry,
   [
    {1,"Magnetmaske"},
    {2,"Sperren"},
    {3,"Entsperren"},
    {4,"Umkehren"},
    {6,"Auswahl gegen Einfluß von Magneten sperren"},
    {7,"Alle gesperrten Elemente der Auswahl entsperren"},
    {8,"Gesperrte und entsperrte Elemente umkehren"},
    {9,"Abwählen"},
    {10,"Gesperrte Element aus aktueller Auswahl entfernen"},
    {11,"Auswählen"},
    {12,"Gesperrte Elemente zur aktuellen Auswahl hinzufügen"}
   ]},
  {view_menu_entry,
   [
    {1,"Magnetmaske zeigen"},
    {2,"Magnetmaske zeigen"}
   ]}
 ]}.
